﻿using Microsoft.Pex.Framework;
using Microsoft.VisualStudio.TestTools.UnitTesting;

namespace SatisfiableChecker
{
    [PexClass, TestClass]
    public partial class UnitTest1
    {
        [PexMethod, SatisfiableChecker]
        public void Foo([PexAssumeNotNull]MyStack ms)
        {
            //SatisfiableHelper.Check(x > 41);
            //SatisfiableHelper.Check(x % 2 == 0 & x % 2 == 1);
            int y = ms.Size;
            SatisfiableHelper.Check(y > 10);            
        }

        [PexMethod, SatisfiableChecker]
        public void PushInt([PexAssumeUnderTest]IntStack target, int value_ren)
        {
            target.PushInt(value_ren);
        }

        [PexMethod, SatisfiableChecker]
        public void PushAInt([PexAssumeUnderTest]ArrayListStack target, int value_ren)
        {
            target.PushInt(value_ren);
        }

        //[PexMethod, SatisfiableChecker]
        //public void Bar(int x)
        //{
        //    if (x < 10)
        //    {
        //        SatisfiableHelper.Check(x > 41);
        //        SatisfiableHelper.Check(x % 2 == 1);
        //    }
        //}
    }


    public class MyStack
    {
        int size;
        public int Size
        {
            get 
            {
                return this.size;
            }

            set
            {
                this.size = value;
            }
        }

        void setSize(int param)
        {
            this.Size = param;
        }
    }
}